﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

namespace SimpleIR
{
	/// <summary>
	/// This class represents a symbolic evaluation stack
	/// </summary>
	public sealed class SymbolicEvalStack
	{
		private readonly List<SymbolicEvalStackTerm> m_stack;

		public SymbolicEvalStack()
		{ this.m_stack = new List<SymbolicEvalStackTerm>(); }

		public SymbolicEvalStack CopyStack()
		{
			SymbolicEvalStack res = new SymbolicEvalStack();
			res.m_stack.AddRange(this.m_stack);

			return res;
		}

		public SymbolicEvalStackTerm PopTerm()
		{
			SymbolicEvalStackTerm tt = this.m_stack[this.m_stack.Count - 1];
			this.m_stack.RemoveAt(this.m_stack.Count - 1);
			return tt;
		}

		public SymbolicEvalStackTerm PeekTerm()
		{ return this.m_stack[this.m_stack.Count - 1]; }

		public void PushTerm(SymbolicEvalStackTerm t)
		{ this.m_stack.Add(t); }

		/// <summary>
		/// Return the symbolic name for the term at position (top - k). I.e. k = 0 gives the stack top.
		/// </summary>
		public SymbolicEvalStackTerm GetTermAtPos(int k)
		{ return this.m_stack[this.m_stack.Count - (k + 1)]; }

		/// <summary>
		/// Return the symbolic name for the term at position (top - k). I.e. k = 0 gives the stack top.
		/// </summary>
		public void SetTermAtPos(int k, SymbolicEvalStackTerm t)
		{ this.m_stack[this.m_stack.Count - (k + 1)] = t; }

		public void ClearEvalStack()
		{ this.m_stack.Clear(); }

		public void SimplifyEvalStack()
		{
			for(int i = 0; i < this.m_stack.Count; ++i)
			{
				if(this.m_stack[i].SymTerm != SymbolicEvalStackTerm.TermTag.UnknownTerm)
					this.m_stack[i] = SymbolicEvalStackTerm.MakeUnknownTerm(this.m_stack[i].SType);
			}
		}
	}

	/// <summary>
	/// A simple struct that represents the name/path for a value in the eval stack (e.g. the symbolic name used to compute it).
	/// </summary>
	public struct SymbolicEvalStackTerm
	{
		public enum TermTag
		{
			UnknownTerm,   //The location is an unknown symbolic term
			Constant,      //The location is a constant value
			Var,           //The location is equal to a local variable
			AddressOfVar,  //The location holds the address of the given local variable
			FieldIndex,    //The location is a field index off a local variable which is a pointer &(x.f)
			VarAndLoad,    //The location is a field load off a local variable which is a pointers (x.f)
			ConstantOne,   //The location is the constant value 1
			IncrementOfVar //The location is the a local variable incremented by a postive amount
		}

		/// <summary>
		/// The type of the stack location
		/// </summary>
		public readonly IRType SType;

		/// <summary>
		/// The symbolic term info
		/// </summary>
		public readonly TermTag SymTerm;

		/// <summary>
		/// The variable name that is the root of the term
		/// </summary>
		public readonly IRVarName TermRoot;

		/// <summary>
		/// The optional access field that we use as an offset (x.f)
		/// </summary>
		public readonly IRMemberField MemberField;

		private SymbolicEvalStackTerm(IRType stype, TermTag tag, IRVarName tr, IRMemberField mf)
		{
			this.SType = stype;
			this.SymTerm = tag;
			this.TermRoot = tr;
			this.MemberField = mf;
		}

		internal static SymbolicEvalStackTerm MakeUnknownTerm(IRType tt)
		{ return new SymbolicEvalStackTerm(tt, TermTag.UnknownTerm, null, null); }

		internal static SymbolicEvalStackTerm PushLocalVar(IRType tt, IRVarName lv)
		{ return new SymbolicEvalStackTerm(tt, TermTag.Var, lv, null); }

		internal static SymbolicEvalStackTerm PushConstantOne(IRType tt)
		{ return new SymbolicEvalStackTerm(tt, TermTag.ConstantOne, null, null); }

		internal static SymbolicEvalStackTerm PushOtherConstant(IRType tt)
		{ return new SymbolicEvalStackTerm(tt, TermTag.Constant, null, null); }

		internal static SymbolicEvalStackTerm PushLocalVarAddr(IRType tt, IRVarName lv)
		{ return new SymbolicEvalStackTerm(tt, TermTag.AddressOfVar, lv, null); }

		internal static SymbolicEvalStackTerm DoIndexOfField(SymbolicEvalStackTerm evst, IRMemberField mf, IRReferenceType rtype)
		{
			if(evst.SymTerm == TermTag.AddressOfVar && evst.MemberField == null)
				return new SymbolicEvalStackTerm(rtype, TermTag.FieldIndex, evst.TermRoot, mf);
			else
				return MakeUnknownTerm(rtype);
		}

		internal static SymbolicEvalStackTerm DoFieldIndirectLoad(IRType tt, SymbolicEvalStackTerm evst)
		{
			if(evst.SymTerm == TermTag.AddressOfVar)
				return new SymbolicEvalStackTerm(tt, TermTag.Var, evst.TermRoot, null);
			else if(evst.SymTerm == TermTag.FieldIndex)
				return new SymbolicEvalStackTerm(tt, TermTag.VarAndLoad, evst.TermRoot, evst.MemberField);
			else
				return MakeUnknownTerm(tt);
		}

		internal static SymbolicEvalStackTerm DoMemberFieldLoad(IRType tt, IRMemberField mf, SymbolicEvalStackTerm evst)
		{
			if(evst.SymTerm == TermTag.Var)
				return new SymbolicEvalStackTerm(tt, TermTag.VarAndLoad, evst.TermRoot, mf);
			else
				return MakeUnknownTerm(tt);
		}

		internal static SymbolicEvalStackTerm DoAdd(SymbolicEvalStackTerm evst1, SymbolicEvalStackTerm evst2)
		{
			if(evst1.SymTerm == TermTag.Var && evst2.SymTerm == TermTag.ConstantOne)
				return new SymbolicEvalStackTerm(evst1.SType, TermTag.IncrementOfVar, evst1.TermRoot, null);
			else if(evst2.SymTerm == TermTag.Var && evst1.SymTerm == TermTag.ConstantOne)
				return new SymbolicEvalStackTerm(evst2.SType, TermTag.IncrementOfVar, evst2.TermRoot, null);
			else
				return MakeUnknownTerm(evst1.SType);
		}

		internal static SymbolicEvalStackTerm ConvertType(IRType tt, SymbolicEvalStackTerm evst)
		{
			return new SymbolicEvalStackTerm(tt, evst.SymTerm, evst.TermRoot, evst.MemberField);
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder(this.SymTerm.ToString() + " of " + this.SType.ToString());

			if(this.TermRoot != null)
			{
				sb.Append(" -- " + this.TermRoot.ToString());

				if(this.MemberField != null)
					sb.Append("." + this.MemberField.FieldName);
			}

			return sb.ToString();
		}
	}
}
